#!/usr/bin/ruby -w

require "set"

# A CNF (conjunctive normal form) formula is a conjunction of clauses, where
# each clause is a conjunction of variables/literals.
class CnfFormula
  attr_reader(:clauses)
  
  def initialize(clauses)
    if clauses.length < 1
      raise ArgumentError.new("Formula must have at least 1 clause")
    end
    @clauses = clauses
  end
  
  def num_clauses
    return @clauses.length
  end
  
  def num_variables
    variables = Set.new
    @clauses.each do |clause|
      clause.variables.each do |var|
        variables.add(var.name)
      end
    end
    return variables.size
  end
  
  def to_s
    formula = "p cnf " + num_variables.to_s + " " + num_clauses.to_s + "\n"
    @clauses.each do |clause|
      formula += clause.to_s
      formula += " 0\n"
    end
    # Replace last " 0\n" with just the newline
    return formula[0, formula.length - 3] + "\n"
  end
end

class CnfClause
  attr_reader(:variables)
	
  def initialize()
    @variables = []    
  end
  
  def add_variable(var)
	if var.kind_of?(CnfVariable)
	  @variables.push(var)
	elsif var.kind_of?(Fixnum)
	  add_variable(CnfVariable.new(var.abs, var < 0))
	else
	  raise ArgumentError.new("Var is not a CnfVariable and not a Fixnum")
	end
  end
  
  def to_s
    clause_string = ""
    @variables.each do |var|
      clause_string += var.to_s
      clause_string += " "
    end
    # Cut off the last space
    return clause_string[0, clause_string.length - 1]
  end
end

class CnfVariable
  attr_reader(:name)
  attr_reader(:negated)
	
  def initialize(name, negated = false)
    name = name.to_i
    if name < 1 || name > 9
      raise ArgumentError.new("Name must be a Fixnum between 1 and 9, is " + name.to_s)
    end
    
    @name = name.to_s
    @negated = negated
  end
  
  def to_s
    if @negated
      return "-" + name
    else
      return name
    end
  end
end
